Proof of Preservation

Proof of preservation will always be on the bit that steps. If in doubt, try inversion.

Canonical Forms Lemma

Proof of Progress

Related Reading

• Type Safety

Cards

Q: What is the Canonical Forms Lemma and how is it proved? A: That if some expression is of a type, the expression must be of a form from a rule that concludes that type. E.g. if $e: num$ then $e=num[n]$. Also need to include types from premises. Proved by inspection.